package org.korifey.ffbdd.api.deprecated;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.Set;

import org.korifey.ffbdd.api.IBddBackend;
import org.korifey.ffbdd.api.INode;
import org.korifey.ffbdd.api.INonterminal;
import org.korifey.ffbdd.api.ITerminal;
import org.korifey.ffbdd.api.op.IBinaryOperation;
import org.korifey.ffbdd.api.op.IOpCache;
import org.korifey.ffbdd.api.op.OperationEnum;

public class Bdd<T> {	
	
	
	static IBddBackend bddBackend;
	static IOpCache opCache;
	static int nextVar = 1;
	
	/*static {
		bddBackend = new BddBackendBitvector();
		((BddBackendBitvector)bddBackend).init(1000000, 1000);
	}*/
	
	public static void setBddBackend(IBddBackend bddBackend) {
		Bdd.bddBackend = bddBackend; 
	}
	
	public static void setOpCache(IOpCache opcache) {
		Bdd.opCache = opcache;
	}
	
	private static INode insertNonterminal(int var, INode one, INode zero) {
		return bddBackend.insertNonterminal(var, one, zero);
	}
	
	private static <E> ITerminal<E> insertTerminal(E value) {
		return bddBackend.insertTerminal(value);
	}
			
	
	
	
	private INode root;	
	
	protected Bdd(INode n) {
		root = n;
	}
		
	
	
	
	@Override
	public int hashCode() {
		return root.hashCode();
	}

	@Override
	public boolean equals(Object obj) {
		if (this == obj)
			return true;
		if (obj == null)
			return false;
		if (getClass() != obj.getClass())
			return false;
		Bdd other = (Bdd) obj;
		if (root != other.root)
			return false;
		return true;
	}

	
	public static <E> Bdd<E> makeConst(E value) {
		return new Bdd(insertTerminal(value));
	}
	
	public static <E> Bdd<E> makeNode(int var, E valueOne, E valueZero, boolean inversed) {
		ITerminal<E> one = insertTerminal(valueOne);
		ITerminal<E> zero = insertTerminal(valueZero);
		INode n = (!inversed)?insertNonterminal(var, one, zero) : insertNonterminal(var, zero, one);
		return new Bdd<E>(n);
	}

	public static int getNextVar() {
		return nextVar;
	}

	public boolean isConst() {
		return root.isTerm();
	}

	public Bdd<T> insertNewList(List<T> consumerResources) {
		int size = consumerResources.size();
		int domlen = 0;
		for (int i=1; i<=size; i*=2) domlen++;
		int[] varidx = new int[domlen];
		boolean[] varval = new boolean[domlen];
		
		for (int i=0; i<domlen; i++) varidx[i] = nextVar++;
		
		Bdd<T> res = this;
		for (int i=0; i<size; i++) {
			res = res.insertElem(consumerResources.get(i), varidx, varval);
			int k = varval.length-1;
			while (varval[k]) varval[k--] = false;
			if (k>=0) varval[k] = true;
		}
		return res;
	}
	
	public Bdd<T> insertElem(T value, int[] varIndex, boolean[] varValue) {
		Bdd<Boolean> elem = makeConst(true);
		for (int i=0; i<varIndex.length; i++) {
			elem = elem.and(makeNode(varIndex[i], true, false, varValue[i]));
		}
		return Bdd.ite(elem, makeConst(value), this);
	}

	
	public Bdd<T> condNE(Bdd<T> bdd, T badval) {
		return Bdd.ite(this.notEquals(bdd), this, makeConst(badval));
	}

	private Bdd<Boolean> notEquals(Bdd<T> bdd) {
		return Bdd.apply(this, bdd, (IBinaryOperation)OperationEnum.NEQ.getOperation());
	}
	

	public Bdd<Boolean> and(Bdd<Boolean> bdd) {
		return Bdd.apply(this, bdd, (IBinaryOperation)OperationEnum.AND.getOperation());
	}
	
	
	
	static Cache<INode> opcache = new Cache(2000000);
	
	
	
	private static <T1,T2,T3> Bdd<T3> apply(Bdd<T1> bdd, Bdd<T2> bdd2, IBinaryOperation<T1,T2,T3> binop) {
		return new Bdd(Bdd._apply(bdd.root, bdd2.root, binop));
	}
		
	private static INode _apply(INode n1, INode n2, IBinaryOperation binop) {
		CacheKey.BinopKey key = new CacheKey.BinopKey(n1, n2, binop);
		if (opcache.contain(key)) return opcache.get(key);
		
		INode res = null;
		if (n1.isTerm() && n2.isTerm()) {
			res = insertTerminal(binop.apply(((ITerminal)n1).getValue(), ((ITerminal)n2).getValue()));
		} else {
			int var = minVar(n1, n2);
			res = insertNonterminal(var,
					_apply(optOne(var, n1), optOne(var, n2), binop), 
					_apply(optZero(var, n1), optZero(var, n2), binop)
					);		
		}
		opcache.put(key, res);
		return res;
	}
	
	
	public static <T> Bdd<T> ite(Bdd<Boolean> cond, Bdd<T> bdd1, Bdd<T> bdd2) {
		return new Bdd(Bdd._ite(cond.root, bdd1.root, bdd2.root));
	}
	
	private static INode optOne(int var, INode n) {
		if (n.isTerm()) return n;
		INonterminal nt = (INonterminal)n;
		if (nt.var() == var) return nt.one();
		else return n;
	}
	
	private static INode optZero(int var, INode n) {
		if (n.isTerm()) return n;
		INonterminal nt = (INonterminal)n;
		if (nt.var() == var) return nt.zero();
		else return n;
	}
	
	private static int optVar(INode n) {
		if (n.isTerm()) return Integer.MAX_VALUE;
		INonterminal nt = (INonterminal)n;
		return nt.var();
	}
	
	private static int minVar(INode n1, INode n2) {
		return Math.min(optVar(n1), optVar(n2));
	}
	private static int minVar(INode n1, INode n2, INode n3) {
		return Math.min(Math.min(optVar(n1), optVar(n2)), optVar(n3));
	}
	
	public static INode _ite(INode cond, INode n1, INode n2) {
		CacheKey.ITEKey key = new CacheKey.ITEKey (cond, n1, n2);
		if (opcache.contain(key)) return opcache.get(key);
		
		INode res;
		if (n1.isTerm() && n2.isTerm() && cond.isTerm()) {
			res = (((ITerminal<Boolean>)cond).getValue()) ? n1 : n2;
		} else {
			int var = minVar(n1, n2, cond);
			res = insertNonterminal(var,
					_ite(optOne(var, cond), optOne(var, n1), optOne(var, n2)), 
					_ite(optZero(var, cond), optZero(var, n1), optZero(var, n2))
					);		
		}
		
		opcache.put(key, res);
		return res;
	}
	
	
	
	
	public String toString() {
		return toString(root, 0);
	}
	
	static String toString(INode n, int lev) {
		String res = "";
		for (int i=0; i<lev; i++) res += "  ";
		if (n.isTerm()) res += "<"+((ITerminal)n).getValue().toString()+">";
		else {
			INonterminal nt = (INonterminal)n;
			res += nt.var() + "\n"+toString(nt.one(), lev+1)+"\n"+toString(nt.zero(), lev+1);
		}
		return res;
	}
	
	
	
	
	
}
